/**
 * The MIT License
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package spoon.smpl;

import fr.inria.controlflow.BranchKind;
import fr.inria.controlflow.ControlFlowNode;
import org.apache.commons.lang3.NotImplementedException;
import spoon.reflect.code.CtBlock;
import spoon.reflect.code.CtExpression;
import spoon.reflect.code.CtInvocation;
import spoon.reflect.code.CtVariableRead;
import spoon.reflect.declaration.CtElement;
import spoon.reflect.declaration.CtMethod;
import spoon.smpl.formula.AllNext;
import spoon.smpl.formula.AllUntil;
import spoon.smpl.formula.And;
import spoon.smpl.formula.BinaryConnective;
import spoon.smpl.formula.Branch;
import spoon.smpl.formula.ExistsNext;
import spoon.smpl.formula.ExistsUntil;
import spoon.smpl.formula.ExistsVar;
import spoon.smpl.formula.Expression;
import spoon.smpl.formula.Formula;
import spoon.smpl.formula.InnerAnd;
import spoon.smpl.formula.MetadataPredicate;
import spoon.smpl.formula.MetavariableConstraint;
import spoon.smpl.formula.MethodHeaderPredicate;
import spoon.smpl.formula.Not;
import spoon.smpl.formula.Optional;
import spoon.smpl.formula.Or;
import spoon.smpl.formula.Proposition;
import spoon.smpl.formula.SequentialOr;
import spoon.smpl.formula.SetEnv;
import spoon.smpl.formula.Statement;
import spoon.smpl.formula.True;
import spoon.smpl.formula.VariableUsePredicate;
import spoon.smpl.operation.Operation;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Deque;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;


/**
 * FormulaCompiler compiles CTL-VW Formulas from a given SmPL-adapted CFG of a method body in
 * the SmPL Java DSL (domain-specific language) of spoon-smpl, as generated by SmPLParser.
 */
public class FormulaCompiler {
	/**
	 * Create a new FormulaCompiler.
	 *
	 * @param cfg        SmPL-adapted CFG to produce formula from
	 * @param metavars   Metavariable names and their constraints
	 * @param operations Map of line-anchored operations
	 */
	public FormulaCompiler(SmPLMethodCFG cfg, Map<String, MetavariableConstraint> metavars, AnchoredOperationsMap operations) {
		this.cfg = cfg;
		this.metavars = metavars;
		this.operations = operations;
	}

	/**
	 * Compile the CTL-VW Formula.
	 *
	 * @return CTL-VW Formula
	 */
	public Formula compileFormula() {
		metavarsToQuantifyOutermost = new ArrayList<>();

		Formula formula = compileFormulaInner(cfg.findNodesOfKind(BranchKind.BEGIN).get(0).next().get(0), null, new ArrayList<>());
		formula = FormulaOptimizer.optimizeFully(formula);

		Collections.sort(metavarsToQuantifyOutermost);
		Collections.reverse(metavarsToQuantifyOutermost);

		for (String var : metavarsToQuantifyOutermost) {
			formula = new ExistsVar(var, formula);
		}

		return formula;
	}

	/**
	 * Compile a CTL-VW Formula.
	 *
	 * @param node        First node of control flow graph to generate formula for
	 * @param cutoffNodes Nodes at which formula compilation should stop
	 * @return CTL-VW Formula
	 */
	private Formula compileFormulaInner(ControlFlowNode node, List<ControlFlowNode> cutoffNodes, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);

		Formula formula;
		Formula innerFormula;
		SmPLMethodCFG.NodeTag tag;

		try {
			tag = (SmPLMethodCFG.NodeTag) node.getTag();
		} catch (ClassCastException e) {
			tag = null;
		}

		if (cutoffNodes != null) {
			for (ControlFlowNode someNode : cutoffNodes) {
				if (someNode == node) {
					return null;
				}
			}
		}

		if (node.getKind() == BranchKind.EXIT) {
			return new Proposition("end");
		} else if (SmPLMethodCFG.isMethodHeaderNode(node)) {
			return compileMethodHeaderFormula(node, cutoffNodes, quantifiedMetavars);
		} else {
			switch (node.next().size()) {
				case 0:
					throw new IllegalArgumentException("Control flow node with no outgoing path");

				case 1:
					switch (node.getKind()) {
						case STATEMENT:
							return compileStatementFormula(node, cutoffNodes, quantifiedMetavars);

						case BLOCK_BEGIN:
							if (isNodeForSmPLJavaDSLMetaElement(node)) {
								return compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);
							}

							if (tag == null) {
								throw new IllegalArgumentException("invalid tag for " + node.getKind().toString()
																	+ " node " + Integer.toString(node.getId()));
							}

							String parentIdVar = "__parent" + Integer.toString((int) tag.getMetadata("parent")) + "__";

							boolean shouldQuantify = !quantifiedMetavars.contains(parentIdVar);

							quantifiedMetavars.add(parentIdVar);

							innerFormula = compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);

							formula = new And(new Proposition(tag.getLabel()),
												new MetadataPredicate(parentIdVar, "parent"));

							if (innerFormula != null) {
								formula = new And(formula,
													connectTail(innerFormula));
							}

							if (shouldQuantify) {
								formula = new ExistsVar(parentIdVar, formula);
								quantifiedMetavars.remove(parentIdVar);
							}

							return formula;

						case CONVERGE:
							if (isNodeForSmPLJavaDSLMetaElement(node)) {
								return compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);
							}

							formula = new Proposition("after");

							innerFormula = compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);

							if (innerFormula == null) {
								return formula;
							} else {
								return new And(formula, connectTail(innerFormula));
							}

						case TRY:
						case CATCH:
							if (tag == null) {
								throw new IllegalArgumentException("invalid tag for " + node.toString());
							}

							formula = new Proposition(tag.getLabel());
							innerFormula = compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);

							return combine(formula, connectTail(innerFormula), And.class);
						default:
							throw new IllegalArgumentException("Unexpected control flow node kind for single successor: " + node.getKind().toString());
					}

				default:
					switch (node.getKind()) {
						case STATEMENT:
							// Will probably need this if adding support for exceptions
							throw new NotImplementedException("Not implemented");

						case BRANCH:
							CtElement statement = node.getStatement();

							if (SmPLJavaDSL.isDotsWithOptionalMatch(statement.getParent())) {
								return compileDotsWithOptionalMatchFormula(node, cutoffNodes, quantifiedMetavars);
							} else if (SmPLJavaDSL.isBeginDisjunction(statement.getParent())) {
								return compileDisjunction(node, cutoffNodes, quantifiedMetavars);
							} else {
								return compileBranchFormula(node, cutoffNodes, quantifiedMetavars);
							}

						default:
							throw new IllegalArgumentException("Unexpected control flow node kind for multiple successors: " + node.getKind().toString());
					}
			}
		}
	}

	/**
	 * Compile a formula for the special method header node.
	 *
	 * @param node        Method header node
	 * @param cutoffNodes Nodes at which formula compilation should stop
	 * @return CTL-VW Formula
	 */
	private Formula compileMethodHeaderFormula(ControlFlowNode node, List<ControlFlowNode> cutoffNodes, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);

		Formula formula;

		if (!(node.getTag() instanceof SmPLMethodCFG.NodeTag)) {
			throw new IllegalArgumentException("invalid tag type for method header node");
		}

		SmPLMethodCFG.NodeTag tag = (SmPLMethodCFG.NodeTag) node.getTag();

		if (!(tag.getAnchor() instanceof CtMethod)) {
			throw new IllegalArgumentException("invalid anchor for method header node");
		}

		if (SmPLJavaDSL.isUnspecifiedMethodHeader(tag.getAnchor())) {
			formula = new Proposition("methodHeader");
		} else {
			formula = new MethodHeaderPredicate((CtMethod<?>) tag.getAnchor(), metavars);
			Set<String> metavarsUsed = ((MethodHeaderPredicate) formula).getMetavarsUsedInHeader();

			quantifiedMetavars.addAll(metavarsUsed);
			metavarsToQuantifyOutermost.addAll(metavarsUsed);
		}

		List<Operation> methodBodyOps = operations.getOperationsAnchoredToMethodBody();

		if (methodBodyOps != null && methodBodyOps.size() > 0) {
			formula = new And(formula, new ExistsVar("_v", new SetEnv("_v", methodBodyOps)));
		}

		return new And(formula, connectTail(compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars)));
	}

	/**
	 * Compile a CTL-VW Formula for a given single-statement single-successor CFG node.
	 *
	 * @param node        A single-statement, single-successor CFG node
	 * @param cutoffNodes Nodes at which formula compilation should stop
	 * @return CTL-VW Formula
	 */
	private Formula compileStatementFormula(ControlFlowNode node, List<ControlFlowNode> cutoffNodes, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);

		if (SmPLJavaDSL.isStatementLevelDots(node.getStatement())) {
			return compileStatementLevelDotsFormula(node, cutoffNodes, quantifiedMetavars);
		} else {
			CtElement statement = node.getStatement();
			Formula formula;

			if (SmPLJavaDSL.isExpressionMatchWrapper(statement)) {
				statement = SmPLJavaDSL.getWrappedElement(statement);
				formula = new Expression(statement, metavars);
			} else {
				formula = new Statement(statement, metavars);
			}

			int line = statement.getPosition().getLine();

			ArrayList<Operation> ops = new ArrayList<>();

			if (operations.containsKey(line)) {
				ops.addAll(operations.get(line));
			}

			if (ops.size() > 0) {
				formula = new And(formula, new ExistsVar("_v", new SetEnv("_v", ops)));
			}

			// Mark first occurences of metavars as quantified before compiling inner formula
			List<String> newMetavars = getUnquantifiedMetavarsUsedIn(statement, quantifiedMetavars);
			quantifiedMetavars.addAll(newMetavars);

			Formula innerFormula = compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);

			if (innerFormula != null) {
				formula = new And(formula, connectTail(innerFormula));
			}

			// Actually quantify the new metavars
			Collections.reverse(newMetavars);

			for (String varname : newMetavars) {
				formula = new ExistsVar(varname, formula);
			}

			return formula;
		}
	}

	/**
	 * Compile a CTL-VW Formula for a given branch statement multi-successor CFG node.
	 *
	 * @param node        A branch statement, multi-successor CFG node
	 * @param cutoffNodes Nodes at which formula compilation should stop
	 * @return CTL-VW Formula
	 */
	private Formula compileBranchFormula(ControlFlowNode node, List<ControlFlowNode> cutoffNodes, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);

		Formula formula;

		CtElement statement = node.getStatement();
		int line = statement.getPosition().getLine();

		formula = new Branch(statement.getParent(), metavars);

		ArrayList<Operation> ops = new ArrayList<>();

		if (operations.containsKey(line)) {
			ops.addAll(operations.get(line));
		}

		if (ops.size() > 0) {
			formula = new And(formula, new ExistsVar("_v", new SetEnv("_v", ops)));
		}

		// Mark first occurences of metavars as quantified before compiling inner formulas
		List<String> newMetavars = getUnquantifiedMetavarsUsedIn(node.getStatement(), quantifiedMetavars);
		quantifiedMetavars.addAll(newMetavars);

		Formula lhs = compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);
		Formula rhs = compileFormulaInner(node.next().get(1), cutoffNodes, quantifiedMetavars);

		if (lhs != null && rhs != null) {
			formula = new And(formula, new And(new ExistsNext(lhs), new ExistsNext(rhs)));
		} else if (lhs != null) {
			formula = new And(formula, new ExistsNext(lhs));
		} else if (rhs != null) {
			formula = new And(formula, new ExistsNext(rhs));
		}

		// Actually quantify the new metavars
		Collections.reverse(newMetavars);

		for (String varname : newMetavars) {
			formula = new ExistsVar(varname, formula);
		}

		return formula;
	}

	/**
	 * Given a Formula compiled starting from a node S different from the CFG start node (i.e one possible tail of some
	 * path starting in some immediate predecessor to S), wrap the Formula in a connector appropriate for connecting it
	 * to the Formula element compiled for said predecessor.
	 * <p>
	 * Essentially, for a given Formula Psi this boils down to choosing from X in {AllNext(Psi), ExistsNext(Psi)}
	 * such that the construction And(Phi, X) is semantically correct in the SmPL context, with Phi being the Formula
	 * element compiled for a predecessor to Psi.
	 * <p>
	 * In the SmPL context the only case where an ExistsUntil appears is for dots using the "when exists" constraint
	 * relaxation, the semantics of which requires the use of the ExistsNext connector rather than the AllNext
	 * connector.
	 *
	 * @param tail Formula tail
	 * @return Tail wrapped in appropriate connector
	 */
	private Formula connectTail(Formula tail) {
		if (tail == null) {
			return null;
		} else if (tail instanceof ExistsUntil) {
			return new ExistsNext(tail);
		} else {
			return new AllNext(tail);
		}
	}

	/**
	 * Get the (non-finalized) shortest path guard formula for the element preceding a given statement-level
	 * dots or dots-with-optional-match operator node.
	 *
	 * @param dotsNode Node of statement-level dots or dots-with-optional-match operator
	 * @return Non-finalized shortest path guard formula for preceding element
	 */
	private Formula getDotsPreGuard(ControlFlowNode dotsNode, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);
		List<ControlFlowNode> prevNodes = dotsNode.prev();

		switch (prevNodes.size()) {
			case 1:
				ControlFlowNode prevNode = prevNodes.get(0);

				switch (prevNode.getKind()) {
					case STATEMENT:
						if (SmPLMethodCFG.isMethodHeaderNode(prevNode)) {
							return null;
						}

						return compileFormulaInner(prevNode, Collections.singletonList(dotsNode), quantifiedMetavars);

					case BLOCK_BEGIN:
						switch (prevNode.prev().size()) {
							case 1:
								return compileFormulaInner(prevNode.prev().get(0), prevNode.prev().get(0).next(), quantifiedMetavars);

							default:
								throw new NotImplementedException("preGuard not implemented for BLOCK_BEGIN with " + Integer.toString(prevNode.prev().size()) + " predecessors");
						}


					case CONVERGE:
						// FIXME: relies on implementation details in spoon-control-flow
						ControlFlowNode branchNode = prevNode.getParent().findNodeById(prevNode.getId() - 1);

						if (SmPLJavaDSL.isBeginDisjunction(branchNode.getStatement().getParent())) {
							// TODO: figure out if a disjunction should generate a guard
							return null;
						} else {
							return compileFormulaInner(branchNode, branchNode.next(), quantifiedMetavars);
						}
					default:
						throw new NotImplementedException("preGuard not implemented for " + prevNode.getKind().toString() + " single predecessor");
				}

			default:
				throw new NotImplementedException("preGuard not implemented for " + prevNodes.size() + " predecessors");
		}
	}

	/**
	 * Get the (non-finalized) shortest path guard formula for the element succeeding a given statement-level
	 * dots or dots-with-optional-match operator node.
	 *
	 * @param dotsNode Node of statement-level dots or dots-with-optional-match operator
	 * @return Non-finalized shortest path guard formula for succeeding element
	 */
	private Formula getDotsPostGuard(ControlFlowNode dotsNode, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);
		List<ControlFlowNode> nextNodes = dotsNode.next();

		if (SmPLJavaDSL.isDotsWithOptionalMatch(dotsNode.getStatement().getParent())) {
			// FIXME: relies on implementation details of ControlFlowBuilder / ControlFlowNode
			// optdots are encoded as an elseless if-statement in the DSL, so pick nextNodes from the .next() of its post-branch convergence node
			nextNodes = dotsNode.getParent().findNodeById(dotsNode.getId() + 1).next();
		}

		switch (nextNodes.size()) {
			case 1:
				ControlFlowNode nextNode = nextNodes.get(0);

				switch (nextNode.getKind()) {
					case STATEMENT:
						return compileFormulaInner(nextNode, nextNode.next(), quantifiedMetavars);

					case CONVERGE:
						return null;

					case EXIT:
						return null;

					default:
						throw new NotImplementedException("postGuard not implemented for " + nextNode.getKind().toString() + " single successor");
				}

			default:
				throw new NotImplementedException("postGuard not implemented for " + nextNodes.size() + " successors");
		}
	}

	/**
	 * Remove all transformation operations from a given Formula.
	 *
	 * @param phi Formula to operate on
	 * @return Formula without transformation operations
	 */
	private static Formula removeOperations(Formula phi) {
		// TODO: might want to replace this with a full visitor that properly removes all ops regardless of nesting
		if (phi == null) {
			return null;
		}

		if (phi instanceof And && ((And) phi).getRhs() instanceof ExistsVar
			&& ((ExistsVar) ((And) phi).getRhs()).getVarName().equals("_v")) {
			return ((And) phi).getLhs();
		} else {
			return phi;
		}
	}

	/**
	 * Find the ID of the immediate parent branch for a given node.
	 *
	 * @param node Node for which to find the ID of the parent branch
	 * @return ID of parent branch, or -1 if the closest parent of the node is the method body
	 */
	private int findParentId(ControlFlowNode node) {
		CtElement element = node.getStatement();
		CtElement parent = element.getParent();

		// iteratively ascend the AST until we either find a branch statement or the method itself
		while (parent instanceof CtBlock<?> || SmPLJavaDSL.isDotsWithOptionalMatch(parent)) {
			parent = parent.getParent();
		}

		if (parent instanceof CtMethod) {
			return -1;
		}

		for (ControlFlowNode otherNode : node.getParent().findNodesOfKind(BranchKind.BRANCH)) {
			SmPLMethodCFG.NodeTag tag = (SmPLMethodCFG.NodeTag) otherNode.getTag();

			if (tag.getAnchor() == parent) {
				return (int) tag.getMetadata("parentId");
			}
		}

		throw new IllegalStateException("impossible situation / malformed cfg");
	}

	/**
	 * Combine two Formulas using a given binary connective.
	 *
	 * @param phi        First Formula
	 * @param psi        Second Formula
	 * @param connective Binary connective
	 * @return A new instance of the binary connective connecting both Formulas, or first (or second) Formula if the second (or first) Formula is null.
	 */
	private Formula combine(Formula phi, Formula psi, Class<? extends BinaryConnective> connective) {
		try {
			if (phi == null) {
				return psi;
			} else if (psi == null) {
				return phi;
			} else {
				return connective.getConstructor(Formula.class, Formula.class).newInstance(phi, psi);
			}
		} catch (Exception e) {
			return null;
		}
	}

	/**
	 * Get the guard Formula for a dots operator. The guard prohibits the operator from leaving its enclosing scope
	 * and optionally constrains the operator to match the shortest path between its surrounding context elements.
	 * The result is a non-finalized (non-negated) guard Formula which should be finalized with a call to
	 * finalizeDotsGuard().
	 *
	 * @param dotsNode     Node representing a dots operator
	 * @param shortestPath Flag indicating whether the guard should enforce the shortest path constraint
	 * @return Non-finalized guard Formula
	 */
	private Formula getDotsGuard(ControlFlowNode dotsNode, boolean shortestPath, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);
		int parentId = findParentId(dotsNode);

		Formula guard = null;

		if (parentId != -1) {
			String parentIdVar = "__parent" + Integer.toString(parentId) + "__";
			guard = new And(new Proposition("after"), new MetadataPredicate(parentIdVar, "parent"));
		}

		if (shortestPath) {
			Formula contextPreGuard = getDotsPreGuard(dotsNode, quantifiedMetavars);
			Formula contextPostGuard = getDotsPostGuard(dotsNode, quantifiedMetavars);

			contextPreGuard = removeOperations(contextPreGuard);
			contextPostGuard = removeOperations(contextPostGuard);

			guard = combine(guard, contextPreGuard, Or.class);
			guard = combine(guard, contextPostGuard, Or.class);
		}

		return guard;
	}

	/**
	 * Finalize a dots guard by negating it (if non-null), or by replacing a null guard with True.
	 *
	 * @param input Non-finalized dots guard Formula
	 * @return Negated input if input is not null, otherwise a Formula "True"
	 */
	private Formula finalizeDotsGuard(Formula input) {
		return input != null ? new Not(input) : new True();
	}

	/**
	 * Check if a given Formula is a Proposition for matching the end (exit) node.
	 *
	 * @param phi Formula to test
	 * @return True if Formula is a Proposition matching the end (exit) node, false otherwise
	 */
	private boolean isEndNodeProposition(Formula phi) {
		return phi instanceof Proposition && ((Proposition) phi).getProposition().equals("end");
	}

	/**
	 * Compile a CTL-VW formula for a statement-level dots operator.
	 *
	 * @param node        Node representing a statement-level dots operator
	 * @param cutoffNodes Nodes at which formula compilation should stop
	 * @return CTL-VW Formula
	 */
	private Formula compileStatementLevelDotsFormula(ControlFlowNode node, List<ControlFlowNode> cutoffNodes, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);
		CtInvocation<?> dots = (CtInvocation<?>) node.getStatement();

		Formula guard = getDotsGuard(node, false == SmPLJavaDSL.hasWhenAny(dots), quantifiedMetavars);
		Formula innerFormula = compileFormulaInner(node.next().get(0), cutoffNodes, quantifiedMetavars);

		if (innerFormula == null) {
			innerFormula = new Proposition("end");
		}

		List<CtElement> whenNotEquals = SmPLJavaDSL.getWhenNotEquals(dots);

		if (whenNotEquals.size() > 0) {
			Iterator<CtElement> it = whenNotEquals.iterator();

			while (it.hasNext()) {
				CtElement neqElement = it.next();

				if (SmPLJavaDSL.isExpressionMatchWrapper(neqElement)) {
					neqElement = SmPLJavaDSL.getWrappedElement(neqElement);
				}

				// TODO: use expression match for variables as well? (--> get rid of VariableUsePredicate)

				if (neqElement instanceof CtVariableRead) {
					guard = combine(guard, new VariableUsePredicate(((CtVariableRead<?>) neqElement).getVariable().getSimpleName(), metavars), Or.class);
				} else if (neqElement instanceof CtExpression) {
					guard = combine(guard, new Expression(neqElement, metavars), Or.class);
				} else {
					throw new NotImplementedException("WhenNotEqual not implemented for " + neqElement.getClass().toString());
				}
			}
		}

		if (whenNotEquals.size() > 0 || !isEndNodeProposition(innerFormula)) {
			guard = combine(guard, new Proposition("unsupported"), Or.class);
		}

		if (SmPLJavaDSL.hasWhenExists(dots)) {
			return new ExistsUntil(finalizeDotsGuard(guard), innerFormula);
		} else {
			return new AllUntil(finalizeDotsGuard(guard), innerFormula);
		}
	}

	/**
	 * Compile a formula for a dots-with-optional-match SmPL construct. This construct is represented in the
	 * SmPL Java DSL as an elseless if-statement with the optional match contained in the body of the then-statement.
	 *
	 * @param node        BRANCH node corresponding to the if-statement of the SmPL Java DSL representation of a
	 *                    dots-with-optional-match SmPL construct
	 * @param cutoffNodes Nodes at which formula compilation should stop
	 * @return CTL-VW Formula
	 */
	private Formula compileDotsWithOptionalMatchFormula(ControlFlowNode node, List<ControlFlowNode> cutoffNodes, List<String> quantifiedMetavars) {
		// TODO: "when any" constraint relaxation
		// TODO: merge the common compilation parts of statement-level and optional-match dots

		quantifiedMetavars = shallowCopy(quantifiedMetavars);
		CtInvocation<?> dots = (CtInvocation<?>) node.getStatement();

		// The SmPL Java DSL construct for dots-with-optional-match is an elseless if, so the branch
		//   node must have exactly two successors where one is a BLOCK_BEGIN node and the other one
		//   is a CONVERGE node

		ControlFlowNode bodyNode = node.next()
										.stream()
										.filter(x -> x.getKind() == BranchKind.BLOCK_BEGIN)
										.findFirst().get()
										.next().get(0); // Move past the BLOCK_BEGIN node

		ControlFlowNode convergenceNode = node.next()
												.stream()
												.filter(x -> x.getKind() == BranchKind.CONVERGE)
												.findFirst().get();

		Formula guard = getDotsGuard(node, true, quantifiedMetavars);
		Formula optionalMatch = compileFormulaInner(bodyNode, Collections.singletonList(convergenceNode), quantifiedMetavars);
		Formula tail = compileFormulaInner(convergenceNode.next().get(0), cutoffNodes, quantifiedMetavars);

		if (tail == null) {
			tail = new Proposition("end");
		}

		if (!isEndNodeProposition(tail)) {
			guard = combine(guard, new Proposition("unsupported"), Or.class);
		}

		// TODO: is there a case where metavariables need to be quantified enclosing the EU/AU here?
		//  maybe if the same unquantified metavariable is used in both the optional match and immediately
		//  in the tail? e.g optionalMatch = ExistsVar(x, ...), tail = ExistsVar(x, ...)
		if (SmPLJavaDSL.hasWhenExists(dots)) {
			return new ExistsUntil(combine(finalizeDotsGuard(guard), new Optional(optionalMatch), And.class), tail);
		} else {
			return new AllUntil(combine(finalizeDotsGuard(guard), new Optional(optionalMatch), And.class), tail);
		}
	}

	/**
	 * Compile a Formula for an SmPL pattern disjunction using the Sequential OR connective.
	 *
	 * @param node        Node representing the start of a pattern disjunction
	 * @param cutoffNodes Node at which formula compilation should stop
	 * @return CTL-VW Formula
	 */
	private Formula compileDisjunction(ControlFlowNode node, List<ControlFlowNode> cutoffNodes, List<String> quantifiedMetavars) {
		quantifiedMetavars = shallowCopy(quantifiedMetavars);
		Deque<ControlFlowNode> workQueue = new ArrayDeque<>();
		List<ControlFlowNode> clauseStartingNodes = new ArrayList<>();

		workQueue.addAll(node.next());

		// Find the starting nodes of each clause
		while (!workQueue.isEmpty()) {
			ControlFlowNode currentNode = workQueue.getFirst();
			workQueue.removeFirst();

			if (currentNode.getKind() == BranchKind.BLOCK_BEGIN || (currentNode.getKind() == BranchKind.BRANCH && SmPLJavaDSL.isContinueDisjunction(currentNode.getStatement().getParent()))) {
				workQueue.addAll(currentNode.next());
			} else if (currentNode.getKind() == BranchKind.STATEMENT || currentNode.getKind() == BranchKind.BRANCH) {
				clauseStartingNodes.add(currentNode);
			}
		}

		SequentialOr formula = new SequentialOr();

		// Compile each clause of the disjunction
		for (ControlFlowNode clauseNode : clauseStartingNodes) {
			formula.add(compileFormulaInner(clauseNode, cutoffNodes, quantifiedMetavars));
		}

		return new InnerAnd(formula);
	}

	/**
	 * Get sorted list of metavariable names referenced in a given AST element.
	 *
	 * @param e Element to scan
	 * @return Sorted list of metavariable names
	 */
	private List<String> getMetavarsUsedIn(CtElement e) {
		List<String> metakeys = new ArrayList<>(metavars.keySet());
		List<String> result = new ArrayList<>(new VariableUseScanner(e, metakeys).getResult().keySet());
		result.retainAll(metakeys);

		Collections.sort(result);

		return result;
	}

	/**
	 * Get sorted list of not-yet-quantified metavariable names referenced in a given AST element.
	 *
	 * @param e Element to scan
	 * @return Sorted list of not-yet-quantified metavariable names
	 */
	private List<String> getUnquantifiedMetavarsUsedIn(CtElement e, List<String> quantifiedMetavars) {
		List<String> result = getMetavarsUsedIn(e);
		result.removeAll(quantifiedMetavars);
		return result;
	}

	/**
	 * Check if a given node is associated with an SmPL Java DSL meta element as opposed to something that should
	 * be directly matched by the formula.
	 *
	 * @param node Node to check
	 * @return True if the node is associated with a meta element, false otherwise
	 */
	private boolean isNodeForSmPLJavaDSLMetaElement(ControlFlowNode node) {
		CtElement element = ((SmPLMethodCFG.NodeTag) node.getTag()).getAnchor();

		if (element instanceof CtBlock<?>) {
			element = element.getParent();
		}

		return SmPLJavaDSL.isBeginDisjunction(element)
				|| SmPLJavaDSL.isContinueDisjunction(element)
				|| SmPLJavaDSL.isDotsWithOptionalMatch(element);
	}

	/**
	 * Create a shallow copy of a given list.
	 *
	 * @param input List to copy
	 * @return Shallow copy of input list
	 */
	private <T> List<T> shallowCopy(List<T> input) {
		return new ArrayList<>(input);
	}

	/**
	 * SmPL-adapted CFG to use for formula generation.
	 */
	private SmPLMethodCFG cfg;

	/**
	 * Metavariable names and their corresponding constraints.
	 */
	private Map<String, MetavariableConstraint> metavars;

	/**
	 * Map of anchored lists of addition operations.
	 */
	private AnchoredOperationsMap operations;

	/**
	 * List of metavariables found during compilation of subformulas that must be quantified at the outermost
	 * nesting level of the formula, i.e enclosing the full formula.
	 */
	private List<String> metavarsToQuantifyOutermost;
}
